Inference at * 1 1 2 
Iof proof for Lemma absval eq:



1. x : 
2. y : 
3. 0  x
4. y < 0
  (x = (-y))  x =  y 

latex

 by ((((((Unfold `pm_equal` 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
C),(first_nat 3:n)) (first_tok :t) inil_term)))) 
CollapseTHEN (Try (D (-1))))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 2:n),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions

, t  T, P  Q, P  Q, P & Q, P  Q, i =  j, P  Q, False, A, A  B